Nuprl Lemma : w-kindtype_wf
0,22
postcript
pdf
i
:Id,
TA
:(Id
Type),
M
:(IdLnk
Id
Type). w-kindtype(
TA
;
M
;
i
)
Knd
Type
latex
Definitions
t
T
,
Type
,
Void
,
x
:
A
B
(
x
)
,
Atom
,
,
{
x
:
A
|
B
(
x
) }
,
,
A
B
,
A
,
P
Q
,
False
,
a
<
b
,
#$n
,
x
:
A
B
(
x
)
,
w-kindtype(
TA
;
M
;
i
)
,
x
.
A
(
x
)
,
kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
;
t
) )
,
x
.
t
(
x
)
,
x
,
y
.
t
(
x
;
y
)
,
if
b
t
else
f
fi
,
a
=
b
,
destination(
l
)
,
x
:
A
.
B
(
x
)
,
f
(
a
)
,
Id
,
IdLnk
,
Knd
Lemmas
Knd
wf
,
IdLnk
wf
,
Id
wf
,
ldst
wf
,
eq
id
wf
,
ifthenelse
wf
,
kindcase
wf
origin
i:Id, TA:(Id
Type), M:(IdLnkIdType). w-kindtype(TA;M;i) 
KndType i:Id, TA:(IdType), M:(IdLnkIdType). w-kindtype(TA;M;i) KndType T
B(x)
B
A
QB(x)
x.A(x)
x. t(x)x,y. t(x;y)
t else f fix:A. B(x)